Struct isotope::term::dynamic::DebugValue [−][src]
Expand description
A debug value with an arbitrary code, type, and name, which dynamically compares by pointer
Fields
name: String
The name of this debug value
code: Code
The code of this debug value
flags: TyckFlags
This value’s flags
Implementations
Create a new debug value with a given code
Create a new debug value with a given name
Create a new debug value TermId
with a given code
Create a new debug value TermId
with a given name
Convert this DebugValue
to a DynamicTerm
Trait Implementations
type Consed = DebugValue
type Consed = DebugValue
The type this conses to
Cons this term within a given context. Return None
if already consed.
Convert this term to it’s own consed type
Whether this term depends on a variable with a given index: if equiv is true, also consider larger variables in the same equivalence class
Get whether a term depends on a variable base <= variable <= ix
Read more
Get the variable filter of this term
This method tests for self
and other
values to be equal, and is used
by ==
. Read more
This method tests for !=
.
type Substituted = DebugValue
type Substituted = DebugValue
The type this substitutes to
Substitute this value recursively
Convert this object’s consed form to it’s substituted form
Shift this term’s variables with index >= base
in a given context
Shift this term’s variables with index >= base
in a given context
Locally typecheck a term: note this is context-independent, without caching
Globally typecheck a term, i.e. typecheck all subterms, without caching
Typecheck this term’s annotation, without caching
Typecheck a term in a given context
Load this term’s current flags
Set this term’s flags. May cause errors if done incorrectly!
Locally typecheck a term: note this is context-independent.
Globally typecheck a term, i.e. typecheck all subterms and their variables
Variable typecheck a term, i.e. typecheck all subterms and their variables.
Typecheck this term’s annotation
Globally typecheck a term and it’s annotation, i.e. typecheck all subterms, annotation subterms, and their variables
Typecheck this term along with it’s variables
Whether this term might be type-checked
type ValueConsed = DebugValue
type ValueConsed = DebugValue
The type of value this is consed to
type ValueSubstituted = DebugValue
type ValueSubstituted = DebugValue
The type of value this is substituted to
Convert this term to a Term
, without any consing
Get the type annotation of this term
Get the index of this term in a program graph. Return None
if this term is unindexed
Get whether this term is a type
Get whether this term is a universe
Get whether this term is a function
Get whether this term is a dependent function type
Coerce this term to another type, with type-checking
fn annotate_unchecked(
&self,
_annot: Annotation,
_ctx: &mut impl ConsCtx + ?Sized
) -> Result<Option<DebugValue>, Error>
[src]
fn annotate_unchecked(
&self,
_annot: Annotation,
_ctx: &mut impl ConsCtx + ?Sized
) -> Result<Option<DebugValue>, Error>
[src]Convert this term to an annotation, with only rudimentary type-checking
Get whether this term is a subtype of another in a given context
Get the hash-code of this term if it was untyped Read more
Compare this term to another within a given context
Apply this value, as a function, to a given vector of arguments in a given context
Returns None
if there is no change. Pops off consumed arguments. Read more
Coerce this term to another type, with type-checking
Coerce this term to another type, with type-checking
Coerce this term to another type, with type-checking
fn annotate_unchecked_id(
&self,
annot: Annotation,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<Option<TermId>, Error>
[src]
fn annotate_unchecked_id(
&self,
annot: Annotation,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<Option<TermId>, Error>
[src]Convert this term to an annotation, with only rudimentary type-checking
fn annotated_unchecked(
&self,
annot: Annotation,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<Self::ValueConsed, Error>
[src]
fn annotated_unchecked(
&self,
annot: Annotation,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<Self::ValueConsed, Error>
[src]Convert this term to an annotation, with only rudimentary type-checking
fn annotated_unchecked_id(
&self,
annot: Annotation,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<TermId, Error>
[src]
fn annotated_unchecked_id(
&self,
annot: Annotation,
ctx: &mut impl ConsCtx + ?Sized
) -> Result<TermId, Error>
[src]Convert this term to an annotation, with only rudimentary type-checking
Get whether this term is a subtype of another in general
fn coerce_annot_ty(
&self,
target: &TermId,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<Option<Annotation>, Error>
[src]
fn coerce_annot_ty(
&self,
target: &TermId,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<Option<Annotation>, Error>
[src]Cast this type into another in a given typing context
Substitute this term’s variables recursively given a context
Substitute this term’s variables given a context
Shift this term’s variables with index >= base
up by n
in a given context
Shift this term’s variables with index >= base
up by n
in a given context
Compare this term to a term ID, within a given context
Cons this term within a given context. Return None
if already consed.
Convert this term to a TermId
within a given context
Get the type of this term, if any
Get the type of this term, if any
Apply this value, as a dependent function type, to a given vector of arguments in a given context
Returns None
if there is no change. Pops off consumed arguments. Read more
Convert this term to a TermId
, without any consing
Clone this term to a TermId
, without any consing
Clone this term to a TermId
within a given context
Clone this term to a Term
without any consing
Shallow cons a term directly into a context
Shallow cons a term directly into a context, cloning if necessary
Convert this term to a normal form
Convert this term a normal form
Convert this term to a normal form, or reduce it up to n
steps
Convert this term a normal form, or reduce it up to n
steps
fn reduce_until(
&self,
reduce: impl ReductionConfig,
until: impl TerminationCondition,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<Option<TermId>, Error>
[src]
fn reduce_until(
&self,
reduce: impl ReductionConfig,
until: impl TerminationCondition,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<Option<TermId>, Error>
[src]Convert this term to a normal form, or reduce it up to n
steps
fn reduced_until(
&self,
reduce: impl ReductionConfig,
until: impl TerminationCondition,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<TermId, Error>
[src]
fn reduced_until(
&self,
reduce: impl ReductionConfig,
until: impl TerminationCondition,
ctx: &mut impl TyCtxMut + ?Sized
) -> Result<TermId, Error>
[src]Convert this term a normal form, or reduce it up to n
steps
Auto Trait Implementations
impl RefUnwindSafe for DebugValue
impl Send for DebugValue
impl Sync for DebugValue
impl Unpin for DebugValue
impl UnwindSafe for DebugValue
Blanket Implementations
Mutably borrows from an owned value. Read more
Borrow an optional value of type T
Cons this term within a given context. Return None
if already consed.
Get the type annotation of this term
Get the index of this term in an isotope
program graph, if any
Get whether this term is a type
Get whether this term is a universe
Get whether this term is in “root form”
Get whether this term is a subtype of another term in a given context
Get whether this term has a universe in all contexts
Get the untyped hash-code of this term
Get the variable filter of this term
Shift this term’s variables with index >= base
up by n
in a given context
Whether this term has a given variable dependency
Whether this term has a given variable dependency below ix
and above base
Load this term’s flags
Set this term’s flags
Compare this term to another dynamic term
Compare this term to another
Compare this term to a term ID
Compare self to key
and return true
if they are equal.